/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.type;

import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Map;
import java.util.Set;

import alloy.ast.Command;
import alloy.ast.Expr;
import alloy.ast.Id;
import alloy.ast.LeafExpr;
import alloy.ast.Location;
import alloy.ast.Module;
import alloy.ast.ModuleInfo;
import alloy.ast.QualifiedName;
import alloy.ast.SigExpr;
import alloy.ast.Signature;
import alloy.util.Dbg;

/**
   Represents the basic type associated with an Alloy signature.  
*/

final public class SigType extends ScopedType implements BasicType {

    /**
     * a mapping from {@link String} type strings
     * to {@link SigType}s, used to maintain the property
     * that only one SigType object is used globally for
     * a given signature type.
     * <em>NOTE:</em> this mapping is modified whenever a new
     * type is created.  Since different dummy types are created
     * for each command, each command keeps its own version of
     * this mapping, and sets this field through {@link #setStringToType}
     * at the appropriate times.
     * @see Command#stringToType
     */
    private static Map _stringToType;

    /** the SigType which is the supertype of this.  If this has no supertype,
	the field is null
     **/
    private SigType _superType;

    /** A set of SigTypes which are the subtypes of this.  If this has no subtypes,
        the set is empty 
    **/
    private Set _subTypes;

    /** the {@link Signature} whose type is this */
    private Signature _sig;

    /** Whether this {@link SigType} is for a {@link Signature}
    whose name is unique among all signatures used in the
    current analysis.  If yes, when displaying the name,
    we do not need to display the path through the modules.
    @see #computeShortTypeNames */
    private boolean _sigNameIsUnique = false;

    /** cached copy of string rep. of type */
    private String _typeString; 

    /** for internal use in instantiating new types */
    private SigType() {
    }

    /**
       @param sig_ signature which is not a subset
     */
    private SigType(Signature sig_) {
        Dbg.check(sig_ != null, "attempt to create SigType with null sig");
        _sig = sig_;
	_subTypes = new HashSet();
	_superType = null;
    }

    /** initialize global state. */
    public static void init() {
        _stringToType = new HashMap();
    }


    /** get the string to type mapping. */
    public static Map getStringToType() {
        return _stringToType;
    }

    /** set the string to type mapping. */
    public static void setStringToType(Map stringToType_) {
        _stringToType = stringToType_;
    }

    /**
     * gets the list of basic SigTypes in current
     * global mapping
     * @return the {@link Collection} of SigTypes
     */
    public static Collection getSigTypes() {
        return _stringToType.values();
    }

    /**
     * gets the list of Strings corresponding to sig types
     * in the current global mapping
     */
    public static Set getSigTypeStrings() {
        return _stringToType.keySet();
    }

    /**
     * gets the SigType object corresponding to some String
     * @return SigType object for String if it exists in current
     * global mapping, <code>null</code> otherwise
     */
    public static SigType getSigTypeForString(String sigTypeString_) {
        return (SigType) _stringToType.get(sigTypeString_);
    }

    /**
     * gets the signature of this
     * @return the Signature
     */
    public Signature getSignature() {
        return _sig;
    }

    /** 
     * gets the supertype of this
     * @return the Supertype of this
     **/
    public SigType getSuperType() {
	return _superType;
    }

    /**
     * gets the subtypes of this
     * @return a Set of subtypes of this
     **/
    public Set getSubTypes() {
	return _subTypes;
    }

    /**
     * adds a SigType to subtypes of this
     * @param subtype_ the subtype of this to be added
     **/
    public void addSubType(SigType subtype_) {
	Dbg.check(subtype_ != null, "attempted to assign a null subtype to " + this);
	Dbg.check(!_subTypes.contains(subtype_), "attempted to assign " + 
		subtype_ + " to " + this + " more than once");
	Dbg.check(subtype_._superType == this, 
		"attempted to assign a subtype to a type other than its supertype");
	// we just assume that subType_ is not a supertype of this!
	_subTypes.add(subtype_);
	// also update the _sig info for this._sig . . .
	_sig.addExtBy(subtype_.getSignature());
        
    }
    
    public String toString() {
	if (_typeString == null) {
	    _typeString = _toString(false);
	}
	return _typeString;
    }
    public String toShortString() {
        return _toString(true);
    }

    /**
     * @return signature name followed by '[', comma-separated types of parameters, ']'
     */
    private String _toString(boolean canShorten_) {
        
	QualifiedName qname = _sig.getName();
        Id id = qname.getId();
        StringBuffer retString =
            new StringBuffer(
                canShorten_ && _sigNameIsUnique ? id.nodeString() : qname.nodeString());
        return retString.toString();
    }

    /** @return a new {@link Expr} corresponding to the set
        associated with the {@link Signature} of this, with this
        as its one {@link BasicType}
     */
    public LeafExpr toExpr() {
        
	QualifiedName sigExprName = _sig.getName();
        SigExpr ret = new SigExpr(Location.UNKNOWN, sigExprName);
        ret.setType(new UnionType(new RelationType(this)));
        return ret;
    }

    public String getAtomName(int atom_) {
        StringBuffer ret = new StringBuffer(toShortString() + "_");
        // add zeros so that alphabetical order is the same as numerical order
        int numZeros = Integer.toString(getScope()).length() - Integer.toString(atom_).length();
        for (int i = 0; i < numZeros; i++) ret.append("0");
        ret.append(atom_);
        return ret.toString();
    }
    
    
    /**
     * @param sigType_ SigType for which we test whether it's a transitive
     * supertype of this
     * @return true if sigType_ is a transitive supertype of this (or sigType_ == this); 
     * otherwise return false
     **/
    public boolean isSubtypeOf(BasicType other) {
	
	if (!(other instanceof SigType)) return false;

	SigType sigType_ = (SigType) other;
	// we can use "==" test because SigTypes are interned

	if (this == sigType_)
	    return true;
	else if ((this._superType == null) || (sigType_._subTypes.isEmpty())) 
	    return false;
	else
	    return (_superType.isSubtypeOf(sigType_));
	
    }

    public boolean isEmpty() {
	return false;

    }
    // STATIC METHODS

   
    /**
     * Computes the intersection of two SigTypes
     * @param st_ SigType
     * @return this if this.isSubsetOf(st_); st2 if st_.isSubsetOf(this); otherwise null
     **/
    public BasicType intersect(BasicType other) {
		
	if (this.isSubtypeOf(other))
	    return this;
	else if (other.isSubtypeOf(this))
	    return other;
	else 
	    //return EmptyType.EMPTY_ERROR_TYPE;
	    return EmptyType.EMPTY_TYPE;    
    }
    
     /**
      * Returns the global sig type associated with sig_ to the 
      * current table, or uses sig_ to create the new global sig 
      * type if it doesn't exist
      * @param sig_ the Signature instance
      * @return the global SigType object
      */
    public static SigType getGlobalSigType(Signature sig_) {
        Dbg.check(sig_ != null, "null sig type");
        SigType retType;// = new SigType(sig_, paramTypes_);
	String typeName = sig_.getName().nodeString();// = retType.toString();
        
	if (_stringToType.containsKey(typeName)) {
	    // return the existing SigType object
	    retType = (SigType) _stringToType.get(typeName);
	} else {
	
	    retType = new SigType(sig_);
	    // if the sig_ extends another Signature, find the
	    // other Signature's type, set it to be retType's supertype
	    // and add retType to supertype's list of subtypes
	    Iterator parent = sig_.getExtends().getSigExprIter();
	    if (parent.hasNext()) {
		SigExpr extendee = (SigExpr)parent.next();
		ModuleInfo moduleInfo = ((Module)sig_.getParent().getParent()).getModuleInfo();
		Signature extSig = moduleInfo.getSignature(extendee.getSig(), null);
		retType._superType = (SigType) _stringToType.get(extSig.getName().toString());
		Dbg.check(retType._superType != null, "attempt to create subtype "
			+ sig_ + " before supertype "+extendee);
		retType._superType.addSubType(retType);
	    } else {
		retType._superType = null;
	    }

	    // add retType to the global map of names to types
	    _stringToType.put(typeName, retType);
	}
        
        return retType;
    }

    /**
     * Tests whether the SigType for the given signature has already been created
     * @param sig_ Signature which will be tested for type existance
     * @return true if a SigType has been assigned to sig_, otherwise returns false
     **/
    public static boolean hasSigType(Signature sig_) {
	return (_stringToType.get(sig_.getName().toString()) != null);
    }

       
    //public class ImproperTypeArgsException extends Exception {}

    //public class NotInstantiableException extends Exception {}

    public static void computeShortSigNames(Set sigTypes) {
        //
        // Compute a list of distinct _signatures_.  We'll
        // compute a short name (if possible) for each
        // signature, and from that derive the short names
        // for the sigTypes (which may be signature
        // instantiations).
        //

        // Gather the list of qualified names which cannot
        // be shortened to just signature name without
        // causing a conflict

        Set conflictNames = new HashSet();
        Map id2qname = new HashMap(); // Id -> QualifiedName
        for (Iterator typeIter = sigTypes.iterator(); typeIter.hasNext();) {
			BasicType basType = (BasicType) typeIter.next();
			if (!(basType instanceof SigType)) {
				continue;
			}        		
			SigType sigType = (SigType) basType;
            Signature sig = sigType.getSignature();
            QualifiedName qname = sig.getName();
            Id id = qname.getId();
            QualifiedName otherName = (QualifiedName) id2qname.get(id);
            if (otherName != null && !qname.equals(otherName))
                conflictNames.add(qname);
            else
                id2qname.put(id, qname);
        }

        // For each SigType, if the qualified name of its signature
        // does not conflict with qualified names of other signatures,
        // we may shorten the qualified name to just the signature name.
        for (Iterator typeIter = sigTypes.iterator(); typeIter.hasNext();) {
			BasicType basType = (BasicType) typeIter.next();
			if (!(basType instanceof SigType)) {
				continue;        	
			}
			SigType sigType = (SigType) basType;
            Signature sig = sigType.getSignature();
            QualifiedName qname = sig.getName();
            Id id = qname.getId();

            sigType._sigNameIsUnique = !conflictNames.contains(qname);
        }
    }
}
